mcsta

Benchmark
Model:embedded v.1 (CTMC)
Parameter(s)MAX_COUNT = 8, T = 12
Property:up_time (exp-reward)
Invocation (default)
mcsta/modest mcsta embedded.jani -E MAX_COUNT=8,T=12 --props up_time -O out.txt Minimal --unsafe --es -S Memory --no-partial-results --epsilon 0 --absolute-epsilon
Execution
Walltime:66.62611985206604s
Return code:0
Note(s):The tool result '47755237358170353/100000000000000' is tagged as incorrect. The reference result is '2183712773184130223598585872047520914488122175606934413903652607811561354541768913273394354150731596243786927117080619972936950933211228822230841017997848035457022536274593694325272937241879112565615452852140040009951110511770453046543602028627759596040876523886281630666909773052679046752196663274749329033495803800223198189977967895274338342496880178318697600470928721863593921368994665022069121923146546749427668869964179406259239705083017079579837316334742438858110597273866404643748527627914035116439622241157884116961455558671646185889750342528436238819022600572834920059281639088233591813067367421725249678046731861054937584690961772718156792664262887588824125917593642808076083267656920293627884196441644507495997854599477443119950196357101319485841624585826437019347618526086759800865732832037553466875466901270734879681407694933108066741180927470524584064389847936646278385013902360895901588016440821591943708613991669538852289652630132790905572134555253789490170005059168185665735052259819770041185303718289878778733406203858246157516444569077120019044145792179148606591105921542067443616924426969193479216839640914514154579330293019916470242897744026812602435662758109157949491075995140783550947236459449746329029215408581508993471668737066067881412164151610804199376708900085509035917841621864138944467290829749417433364929282708907841113027796302533141416770846531202150706514206313094666476596182227170154073034763886586094848742289864106641847262258742294448432880789623129784063411053896323208255462396749474153327589093919489124624553290752885960034489080881223998694665884845850447400494028940797032167745880449766472598409304959825700121500595149639222970342012823184365995869663223168776955822675915520168/4572718918340297992861016207266988509138560572823306848829665424299052227511873796991915409911235818972613004530700672685720698204908764538720326409442926127700951433649408201112092564941380998921576941109250837022494566413393941205188626245721168194140412481054847774404826156318173828592036089336096893561020367354804146432102768640678989122018616511998302777619511228565811485630854571393462819833401567338208035372513671797820811573609314840372672325014146693231179799484153817835593205819002122730433616769967049004357596176219036811262970850919468802314953770502798139191686172212028575730678568621667225640320101421011723756204037351428553435160154128692425948580716062203995704926949659596847047937901467330759606876888282528724729065409076658690813670837079680607659220497177491416940645062309893908652700575386295070426625114918423310586794730384254548668064566827365948822329779522453464872939600768481953319487750588147872980488463406012059924520051494441241400216424433553966775513192672039779506357066648405600713809047919861717117847607341961357554333526306960152722611944383372658119891157778850950172371721016793258709192064299305689622465056677801811031340215436851137792601061271941765262648293155902813064195440251739408021071721765433252009902890909464534701229221329432016138637206311482312570698044605998411197506803148471038371352304706209604224183783179520545733608106657737510279107506655719879117689898747777725608137653857013035855106110221663018957239214900397934041851769373159388703677025445608492463824370974258226639989548083202480591870877671674507734785725257431651992424103523845692631201850480374173032425261397494887570649149902839082330582151102087170601721708405579348599375587665625' (approx. 477.55237358361944) which means a relative error of '4.01195578096237e-12' which is larger than the goal precision '1e-14'.
Relative Error:4.01195578096237e-12
Log
embedded.jani:model: info: embedded is a CTMC model.
embedded.jani: info: Need 16 bytes per state.
embedded.jani: info: Explored 5820 states for MAX_COUNT=8, T=12.0.

Peak memory usage: 55 MB
Analysis results for embedded.jani
Experiment MAX_COUNT=8, T=12.0

+ State space exploration
  State size:  16 bytes
  States:      5820
  Transitions: 5820
  Branches:    16788
  Rate:        83143 states/s
  Time:        0.1 s

+ Property up_time
  Value:  477.55237358170353
  Bounds: [477.55237358170353, 477.55237358170353]
  Time:   66.0 s

  + Precomputations
    Min. prob. 0 states:          0
    Time for min. prob. 0 states: 0.0 s
    Min. prob. 1 states:          5820
    Time for min. prob. 1 states: 0.0 s

  + Essential states
    Iterations:       1
    Essential states: 2666
    Transitions:      2666
    Branches:         13634
    Time:             0.0 s

  + Value iteration
    Final error: 0
    Iterations:  438610
    Time:        66.0 s

Exported results to file "/out.txt".
STDERR
The Modest Toolset (www.modestchecker.net), version v3.1.42-gb5e9d523c.